* Step 1: Bounds WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: U11(mark(X1),X2,X3) -> mark(U11(X1,X2,X3)) U11(ok(X1),ok(X2),ok(X3)) -> ok(U11(X1,X2,X3)) U12(mark(X1),X2,X3) -> mark(U12(X1,X2,X3)) U12(ok(X1),ok(X2),ok(X3)) -> ok(U12(X1,X2,X3)) U13(mark(X1),X2,X3) -> mark(U13(X1,X2,X3)) U13(ok(X1),ok(X2),ok(X3)) -> ok(U13(X1,X2,X3)) U14(mark(X1),X2,X3) -> mark(U14(X1,X2,X3)) U14(ok(X1),ok(X2),ok(X3)) -> ok(U14(X1,X2,X3)) U15(mark(X1),X2) -> mark(U15(X1,X2)) U15(ok(X1),ok(X2)) -> ok(U15(X1,X2)) U16(mark(X)) -> mark(U16(X)) U16(ok(X)) -> ok(U16(X)) U21(mark(X1),X2) -> mark(U21(X1,X2)) U21(ok(X1),ok(X2)) -> ok(U21(X1,X2)) U22(mark(X1),X2) -> mark(U22(X1,X2)) U22(ok(X1),ok(X2)) -> ok(U22(X1,X2)) U23(mark(X)) -> mark(U23(X)) U23(ok(X)) -> ok(U23(X)) U31(mark(X1),X2) -> mark(U31(X1,X2)) U31(ok(X1),ok(X2)) -> ok(U31(X1,X2)) U32(mark(X)) -> mark(U32(X)) U32(ok(X)) -> ok(U32(X)) U41(mark(X)) -> mark(U41(X)) U41(ok(X)) -> ok(U41(X)) U51(mark(X1),X2) -> mark(U51(X1,X2)) U51(ok(X1),ok(X2)) -> ok(U51(X1,X2)) U52(mark(X1),X2) -> mark(U52(X1,X2)) U52(ok(X1),ok(X2)) -> ok(U52(X1,X2)) U61(mark(X1),X2,X3) -> mark(U61(X1,X2,X3)) U61(ok(X1),ok(X2),ok(X3)) -> ok(U61(X1,X2,X3)) U62(mark(X1),X2,X3) -> mark(U62(X1,X2,X3)) U62(ok(X1),ok(X2),ok(X3)) -> ok(U62(X1,X2,X3)) U63(mark(X1),X2,X3) -> mark(U63(X1,X2,X3)) U63(ok(X1),ok(X2),ok(X3)) -> ok(U63(X1,X2,X3)) U64(mark(X1),X2,X3) -> mark(U64(X1,X2,X3)) U64(ok(X1),ok(X2),ok(X3)) -> ok(U64(X1,X2,X3)) isNat(ok(X)) -> ok(isNat(X)) isNatKind(ok(X)) -> ok(isNatKind(X)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) proper(0()) -> ok(0()) proper(tt()) -> ok(tt()) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) - Signature: {U11/3,U12/3,U13/3,U14/3,U15/2,U16/1,U21/2,U22/2,U23/1,U31/2,U32/1,U41/1,U51/2,U52/2,U61/3,U62/3,U63/3,U64/3 ,isNat/1,isNatKind/1,plus/2,proper/1,s/1,top/1} / {0/0,active/1,mark/1,ok/1,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {U11,U12,U13,U14,U15,U16,U21,U22,U23,U31,U32,U41,U51,U52 ,U61,U62,U63,U64,isNat,isNatKind,plus,proper,s,top} and constructors {0,active,mark,ok,tt} + Applied Processor: Bounds {initialAutomaton = minimal, enrichment = match} + Details: The problem is match-bounded by 2. The enriched problem is compatible with follwoing automaton. 0_0() -> 2 0_1() -> 3 U11_0(2,2,2) -> 1 U11_1(2,2,2) -> 3 U12_0(2,2,2) -> 1 U12_1(2,2,2) -> 3 U13_0(2,2,2) -> 1 U13_1(2,2,2) -> 3 U14_0(2,2,2) -> 1 U14_1(2,2,2) -> 3 U15_0(2,2) -> 1 U15_1(2,2) -> 3 U16_0(2) -> 1 U16_1(2) -> 3 U21_0(2,2) -> 1 U21_1(2,2) -> 3 U22_0(2,2) -> 1 U22_1(2,2) -> 3 U23_0(2) -> 1 U23_1(2) -> 3 U31_0(2,2) -> 1 U31_1(2,2) -> 3 U32_0(2) -> 1 U32_1(2) -> 3 U41_0(2) -> 1 U41_1(2) -> 3 U51_0(2,2) -> 1 U51_1(2,2) -> 3 U52_0(2,2) -> 1 U52_1(2,2) -> 3 U61_0(2,2,2) -> 1 U61_1(2,2,2) -> 3 U62_0(2,2,2) -> 1 U62_1(2,2,2) -> 3 U63_0(2,2,2) -> 1 U63_1(2,2,2) -> 3 U64_0(2,2,2) -> 1 U64_1(2,2,2) -> 3 active_0(2) -> 2 active_1(2) -> 4 active_2(3) -> 5 isNat_0(2) -> 1 isNat_1(2) -> 3 isNatKind_0(2) -> 1 isNatKind_1(2) -> 3 mark_0(2) -> 2 mark_1(3) -> 1 mark_1(3) -> 3 ok_0(2) -> 2 ok_1(3) -> 1 ok_1(3) -> 3 ok_1(3) -> 4 plus_0(2,2) -> 1 plus_1(2,2) -> 3 proper_0(2) -> 1 proper_1(2) -> 4 s_0(2) -> 1 s_1(2) -> 3 top_0(2) -> 1 top_1(4) -> 1 top_2(5) -> 1 tt_0() -> 2 tt_1() -> 3 * Step 2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: U11(mark(X1),X2,X3) -> mark(U11(X1,X2,X3)) U11(ok(X1),ok(X2),ok(X3)) -> ok(U11(X1,X2,X3)) U12(mark(X1),X2,X3) -> mark(U12(X1,X2,X3)) U12(ok(X1),ok(X2),ok(X3)) -> ok(U12(X1,X2,X3)) U13(mark(X1),X2,X3) -> mark(U13(X1,X2,X3)) U13(ok(X1),ok(X2),ok(X3)) -> ok(U13(X1,X2,X3)) U14(mark(X1),X2,X3) -> mark(U14(X1,X2,X3)) U14(ok(X1),ok(X2),ok(X3)) -> ok(U14(X1,X2,X3)) U15(mark(X1),X2) -> mark(U15(X1,X2)) U15(ok(X1),ok(X2)) -> ok(U15(X1,X2)) U16(mark(X)) -> mark(U16(X)) U16(ok(X)) -> ok(U16(X)) U21(mark(X1),X2) -> mark(U21(X1,X2)) U21(ok(X1),ok(X2)) -> ok(U21(X1,X2)) U22(mark(X1),X2) -> mark(U22(X1,X2)) U22(ok(X1),ok(X2)) -> ok(U22(X1,X2)) U23(mark(X)) -> mark(U23(X)) U23(ok(X)) -> ok(U23(X)) U31(mark(X1),X2) -> mark(U31(X1,X2)) U31(ok(X1),ok(X2)) -> ok(U31(X1,X2)) U32(mark(X)) -> mark(U32(X)) U32(ok(X)) -> ok(U32(X)) U41(mark(X)) -> mark(U41(X)) U41(ok(X)) -> ok(U41(X)) U51(mark(X1),X2) -> mark(U51(X1,X2)) U51(ok(X1),ok(X2)) -> ok(U51(X1,X2)) U52(mark(X1),X2) -> mark(U52(X1,X2)) U52(ok(X1),ok(X2)) -> ok(U52(X1,X2)) U61(mark(X1),X2,X3) -> mark(U61(X1,X2,X3)) U61(ok(X1),ok(X2),ok(X3)) -> ok(U61(X1,X2,X3)) U62(mark(X1),X2,X3) -> mark(U62(X1,X2,X3)) U62(ok(X1),ok(X2),ok(X3)) -> ok(U62(X1,X2,X3)) U63(mark(X1),X2,X3) -> mark(U63(X1,X2,X3)) U63(ok(X1),ok(X2),ok(X3)) -> ok(U63(X1,X2,X3)) U64(mark(X1),X2,X3) -> mark(U64(X1,X2,X3)) U64(ok(X1),ok(X2),ok(X3)) -> ok(U64(X1,X2,X3)) isNat(ok(X)) -> ok(isNat(X)) isNatKind(ok(X)) -> ok(isNatKind(X)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) proper(0()) -> ok(0()) proper(tt()) -> ok(tt()) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) - Signature: {U11/3,U12/3,U13/3,U14/3,U15/2,U16/1,U21/2,U22/2,U23/1,U31/2,U32/1,U41/1,U51/2,U52/2,U61/3,U62/3,U63/3,U64/3 ,isNat/1,isNatKind/1,plus/2,proper/1,s/1,top/1} / {0/0,active/1,mark/1,ok/1,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {U11,U12,U13,U14,U15,U16,U21,U22,U23,U31,U32,U41,U51,U52 ,U61,U62,U63,U64,isNat,isNatKind,plus,proper,s,top} and constructors {0,active,mark,ok,tt} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))